r:. (qpositive(r))  0 < r 

latex

Definitions

{T}, i <z j, ff, tt, if b then t else f fi , b, A, T, r - s, True, x. t(x), x:A. B(x), P  Q, P  Q, P  Q, P & Q, , t  T, t.1, q_le(r;s), t.2, , gset, , x f y, a < b, goset, a <p b, <+>, a < b, r < s, P  Q, qpositive(r), False, x(s), S  T

Lemmas

qmul wf, qminus positive, mon ident q, qadd comm q, qmul zero qrng, qadd wf, bool wf, true wf, squash wf, not functionality wrt iff, assert of bnot, assert-qeq, or functionality wrt iff, assert of bor, and functionality wrt iff, assert of band, iff transitivity, iff functionality wrt iff, all functionality wrt iff, not wf, bnot wf, qeq wf2, int inc rationals, qsub wf, bor wf, band wf, qpositive wf, assert wf, iff wf, rationals wf